L: List, a:. 0<||L||  (imax-list(L)a  (bL. ba)) 

latex

Definitions	imax(a;b), Prop, A, False, imax-list(L), , ||as||, ij, P  Q, P  Q, P  Q, xL. P(x), AB, x. t(x), t  T, {T}, x:A. B(x), P & Q
Lemmas	l all wf, le wf, guard wf, imax lb, and functionality wrt iff, l all cons, length wf1, non neg length, length cons, l all nil, imax-list wf, imax wf, iff functionality wrt iff, length wf2, nat wf, nat properties, ge wf